Who deems these checks unnecessary? If we want a function/method to be duck-typed, I believe we should be allowed to do so. Duck-typing has been the design paradigm preached by the Python community since I can remember and it is a feature, not a bug.

I agree that we should not drop dynamic type checks because of adding static typing. When not using an editor supporting this (you have no idea how many students edit their code in whatever the system offers), there should still be sensible error messages, not the code crashing later with a seemingly unrelated error message.

If nothing else, this will probably reduce the number of issues opened that boils down to the user doing something wrong.

The checks are necessary in user-facing functions but should not be necessary in much of the internal code if a static checker can verify correctness.

Note also that if the type hints are used consistently on user facing functions then an editor like vscode will already warn the user about passing the wrong type into a function before the code even runs.

Python allows to inspect type annotations in runtime

def square(x: int):
    return x * x

square.__annotations__
# {'x': int}

such that we can implement something like @validate such that

# Function for users that raises on isinstance(x, int)
@validate
def square(x: int):
    return x * x

# Function for internal use
def square(x: int):
    return x * x

So even if we want to do runtime validation,
It should be better done like above, than repeating isinstance checks manually,
which often makes the code more complicated with validation code.

I totally agree. Just wanted to point out that not all people use editors with type hinting (and/or do not understand how to benefit from them).

not all people use editors with type hinting

Agreed. I make very heavy use of ipython for example which does not support this.

Note though that the sentence in the PEP that we are all commenting on here explicitly says (emphasis added):

For functions, classes, and modules INTERNALLY used by SymPy that currently feature unnecessary dynamic type checks, a shift towards static typing should be promoted.

The example here is a good one:
https://github.com/sympy/sympy/blob/b0dcb5af49e7289680d9789d292197675e40490d/sympy/polys/polyclasses.py#L167-L171
In gh-25651 I found bugs by enabling that check. The check is too expensive to be used at runtime though so it was commented out before merge. Almost everything that it checks is something that could be verified by a static type checker but doing that check at runtime means recursively calling isinstance down through a potentially large data structure. The class in question is purely internal and not something that any ordinary SymPy user would ever see directly.

Note also that just attempting to verify that the codebase does indeed only use those types in this particular function is something that consumed development time. The whole PR gh-25651 would be completely unnecessary if the code in question just used type hints but as it is if I want to verify what the types are than I have to add runtime checks and ensure that the entire CI test suite completes successfully (and then fix the bugs that show up).

This is a potentially compelling statement. If there were some real world metrics that show how much a large codebase like SymPy could be sped up by removing all runtime checks and moving to a linting-based type checking procedure, then that would help convince us of any need to do such a radical change.

As I understand though, the speed bottlenecks in SymPy are not due to large numbers of runtime checks but due to inefficient symbolic algorithms.

There can be some discussions about how checking list[list[int]] in runtime could be avoided in polynomial systems, and can be replaced by static typing.

https://github.com/sympy/sympy/blob/b0dcb5af49e7289680d9789d292197675e40490d/sympy/polys/polyclasses.py#L167-L171

As @sylee957 notes it is not just about speed bottlenecks because in many cases the checking is not done to avoid the slowdowns that it would cause. Then the cost of not checking is bugs, debugging etc rather then any immediate measurable slowness. Static type checking can reduce certain types of bugs without causing runtime slowdown.